\begin{tabbing}
es{-}independent(${\it es}$;$i$;$k$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$s_{1}$:($x$:Id$\rightarrow$es{-}vartype(${\it es}$; $i$; $x$)), $s_{2}$:($x$:Id$\rightarrow$es{-}vartype(${\it es}$; $i$; $x$)).\+
\\[0ex]es{-}x{-}equiv(${\it es}$;$i$;$x$;$s_{1}$;$s_{2}$)
\\[0ex]$\Rightarrow$ \=(\=$\forall$$v$:es{-}kindtype(${\it es}$;$i$;$k$).\+\+
\\[0ex]es{-}x{-}equiv(${\it es}$;$i$;$x$;es{-}trans(${\it es}$;$i$)($k$,$v$,$s_{1}$);es{-}trans(${\it es}$;$i$)($k$,$v$,$s_{2}$))
\\[0ex]\& es{-}send(${\it es}$;$i$)($k$,$v$,$s_{1}$) $=$ es{-}send(${\it es}$;$i$)($k$,$v$,$s_{2}$) $\in$ es{-}Msg(${\it es}$) List)
\-\\[0ex]\& (\=islocal($k$)\+
\\[0ex]$\Rightarrow$ \=es{-}choose(${\it es}$;$i$)(act($k$),$s_{1}$)\+
\\[0ex]$=$
\\[0ex]es{-}choose(${\it es}$;$i$)(act($k$),$s_{2}$)
\\[0ex]$\in$ es{-}kindtype(${\it es}$;$i$;$k$)+Unit)
\-\-\-\-
\end{tabbing}